|
|
|
UniTESK is a technology of software testing based on formal specifications. Specifications are written using specialized extensions of traditional programming languages. Our advanced mathematical algorithms enable automated generation of test sequences from specifications, that ensure reliable testing of system behavior with required coverage.
We developed specification extensions for C, C++, C#, and Java programming languages, and tools that support UniTESK technology for the mentioned languages. Besides, we provide a number of services in technology deployment, users training and user support.
|
|
Read more...
|
|
|
Monday, 03 March 2014 |
|
 
Researches of the Software Engineering Department have taken part in Embedded World 2014 in cooperation with Open Source Automation Development Lab (OSADL) on 25-27 February, Nuremberg, Germany.
At the exhibition ISPRAS presented tools and technologies for verification and testing of software and hardware. For Linux kernel space verification we presented: - Linux Driver Verification Tools complementing static analysis tools using advanced verification techniques that provide extra precision and depth of source code analysis.
- KEDR framework facilitating dynamic (runtime and post factum) analysis of Linux kernel modules including device drivers, file systems, etc. As a part of framework it includes Leak Checker and Fault Simulator tools.
- Race Hound - a run-time race condition detection tool for the Linux kernel.
- Linux File System Verification project providing exhaustive test suites for Linux file system drivers.
For testing hardware models we presented: - C++TESK - an open-source C++-toolkit aimed to facilitate functional verification of Register-Transfer-Level hardware designs.
- MicroTESK - a reconfigurable (retargetable and extendable) model-based test program generator for microprocessors and other programmable devices.
Also we demonstrated the following test suites:
- Test suite for kernel interfaces of ARINC-653 real-time operating systems for on-board avionics.
- "Mathematics" test suite for mathematical functions of POSIX/IEEE-754/ISO 60559:2011 specifications.
- LSB certification tests aimed to check if system libraries meet the requirements of Linux Standard Base.
|
|
|
Design Automation Conference 2013 |
|
Monday, 10 June 2013 |
On June, 2-6 research workers of the Software Engineering Department Mikhail Chupilko, Andrey Tatarnikov and Aleksey Kamkin attended the University Booth at the Design Automation Conference held in Austin, TX, USA. They defended workshop report on theme “C++TESK and MicroTESK Hardware Verification Toolkits”.
More information is available here. |
|
|
Saturday, 01 June 2013 |
The 7th Spring/Summer Young Researcher’ Colloquium on Software Engineering (SYRCoSE 2013) was held in Kazan, Russia in May 30-31, 2013. The event was organized by Institute for System Programming of RAS, Saint-Petersburg State University and Kazan National Research Technical University named after A.N. Tupolev (KNRTU-KAI), former Kazan Aviation Institute (KAI). It was supported by Intel, Russian Foundation for Basic Research and Nizhny Novgorod Foundation for Education and Research Assistance.
Mikhail Chupilko, Alexander Protsenko made report on theme “Recognition and Explanation of Incorrect Behavior in Simulation-Based Hardware Verification”. Alexander Kamkin, Tatiana Sergeeva (Institute for System Programming of RAS), Andrei Tatarnikov and Artemiy Utekhin (Moscow State University) made report on theme “MicroTESK: An Extendable Framework for Test Program Generation“. Ilja Zakharov, Vadim Mutilin, Eugene Novikov and Alexey Khoroshilov made report on theme “Generating Environment Model for Linux Device Drivers“. Nikita Komarov made report on theme “On the Implementation of Data-Breakpoints Based Race Detection for Linux Kernel Modules“.
More information is available here. |
|
|
